Nuprl Lemma : w-act-not-null
11,40
postcript
pdf
the_w
:World,
e
:E.
(
isnull(act(
e
)))
latex
Definitions
x
:
A
.
B
(
x
)
,
A
,
t
T
,
P
Q
,
False
,
Lemmas
w-act
wf
,
w-action
wf
,
w-loc
wf
,
not
wf
,
assert
wf
,
w-isnull
wf
,
w-E
wf
,
world
wf
origin
the_w:World, e:E. 
(
isnull(act(e))) the_w:World, e:E. (isnull(act(e))) x:A. B(x)A
T
Q